1 /-
2 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 Parallel computation of a computable sequence of computations by
7 a diagonal enumeration.
8 The important theorems of this operation are proven as
9 terminates_parallel and exists_of_mem_parallel.
10 (This operation is nondeterministic in the sense that it does not
11 honor sequence equivalence (irrelevance of computation time).)
12 -/
13 import data.seq.wseq
src └───────────┘
14 universes u v
15
16 namespace computation
17 open wseq
18 variables {α : Type u} {β : Type v}
19
20 def parallel.aux2 : list (computation α) → α ⊕ list (computation α) :=
id └──┘ └─────────┘ ┴ ┴ ┴ └──┘ └─────────┘ ┴
src └──┘ └─────────┘ ┴ └──┘ └─────────┘
typ └──┘ └─────────┘ ┴ ┴ ┴ └──┘ └─────────┘ ┴
doc └─────────┘ └─────────┘
21 list.foldr (λc o, match o with
id └────────┘ ┴ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴ ┴
22 | sum.inl a := sum.inl a
id └─────┘ ┴ └─────┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘
23 | sum.inr ls := rmap (λ c', c' :: ls) (destruct c)
id └─────┘ └┘ └──┘ └┘ └┘ └┘ └──────┘ ┴
src └─────┘ └──┘ └┘ └──────┘
typ └─────┘ └┘ └──┘ └┘ └┘ └┘ └──────┘ ┴
doc └──┘ └──────┘
24 end) (sum.inr [])
id └─────┘ └┘
src └─────┘ └┘
typ └─────┘ └┘
25
26 def parallel.aux1 : list (computation α) × wseq (computation α) →
id └──┘ └─────────┘ ┴ ┴ └──┘ └─────────┘ ┴ ┴
src └──┘ └─────────┘ ┴ └──┘ └─────────┘
typ └──┘ └─────────┘ ┴ ┴ └──┘ └─────────┘ ┴ ┴
doc └─────────┘ └──┘ └─────────┘
27 α ⊕ list (computation α) × wseq (computation α)
id ┴ ┴ └──┘ └─────────┘ ┴ ┴ └──┘ └─────────┘ ┴
src ┴ └──┘ └─────────┘ ┴ └──┘ └─────────┘
typ ┴ ┴ └──┘ └─────────┘ ┴ ┴ └──┘ └─────────┘ ┴
doc └─────────┘ └──┘ └─────────┘
28 | (l, S) := rmap (λ l', match seq.destruct S with
id ┴┴ ┴ └──┘ └┘ └──────────┘
src ┴ └──┘ └──────────┘
typ ┴┴ ┴ └──┘ └┘ └──────────┘
doc └──┘ └──────────┘
29 | none := (l', nil)
id └──┘ ┴└┘ └─┘
src └──┘ ┴ └─┘
typ └──┘ ┴└┘ └─┘
doc └─┘
30 | some (none, S') := (l', S')
id └──┘ ┴└──┘ └┘ ┴└┘
src └──┘ ┴└──┘ ┴
typ └──┘ ┴└──┘ └┘ ┴└┘
31 | some (some c, S') := (c::l', S')
id ┴└──┘ ┴ └┘ ┴ └┘└┘
src ┴└──┘ ┴ └┘
typ ┴└──┘ ┴ └┘ ┴ └┘└┘
32 end) (parallel.aux2 l)
id └───────────┘
src └───────────┘
typ └───────────┘
33
34 /-- Parallel computation of an infinite stream of computations,
35 taking the first result -/
36 def parallel (S : wseq (computation α)) : computation α :=
id └──┘ └─────────┘ ┴ └─────────┘ ┴
src └──┘ └─────────┘ └─────────┘
typ └──┘ └─────────┘ ┴ └─────────┘ ┴
doc └──┘ └─────────┘ └─────────┘
37 corec parallel.aux1 ([], S)
id └───┘ └───────────┘ ┴└┘ ┴
src └───┘ └───────────┘ ┴└┘
typ └───┘ └───────────┘ ┴└┘ ┴
doc └───┘
38
39 theorem terminates_parallel.aux : ∀ {l : list (computation α)} {S c},
id └──┘ └─────────┘ ┴ ┴ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴ ┴ ┴
doc └─────────┘
40 c ∈ l → terminates c → terminates (corec parallel.aux1 (l, S)) :=
id ┴ ┴ ┴ └────────┘ ┴ └────────┘ └───┘ └───────────┘ ┴┴ ┴
src ┴ └────────┘ └────────┘ └───┘ └───────────┘ ┴
typ ┴ ┴ ┴ └────────┘ ┴ └────────┘ └───┘ └───────────┘ ┴┴ ┴
doc └────────┘ └────────┘ └───┘
41 begin
st └─────
42 have lem1 : ∀ l S, (∃ (a : α), parallel.aux2 l = sum.inl a) →
id ┴ ┴ ┴ └───────────┘ ┴ └─────┘
src └──────────┘ └──┘ ┴ ┴└────┘ ┴┴┴└───────────┘┴ ┴┴┴└─────┘┴ └┘ └
typ └──────────┘ └──┘ ┴ ┴└────┘┴┴┴┴└───────────┘┴ ┴┴┴└─────┘┴ └┘ └
doc └──────────┘ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
txt └──────────┘ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
par └──────────┘ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
pid └───────┘└─┘ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
st ────────────────────────────────────────────────────────────────
43 terminates (corec parallel.aux1 (l, S)),
id └────────┘ └───┘ └───────────┘ ┴
src ───┘└────────┘┴ └───┘┴└───────────┘┴┴ └┘ └┘
typ ───┘└────────┘┴ └───┘┴└───────────┘┴┴ └┘ └┘
doc ───┘└────────┘┴ └───┘┴ ┴ └┘ └┘
txt ───┘ ┴ ┴ ┴ └┘ └┘
par ───┘ ┴ ┴ ┴ └┘ └┘
pid ───┘ ┴ ┴ ┴ └┘ └┘
st ──────────────────────────────────────────┘└─
44 { intros l S e, cases e with a e,
id ┴
src └──────────┘ └────┘ └───────┘
typ └──────────┘ └────┘┴└───────┘
doc └──────────┘ └────┘ └───────┘
txt └──────────┘ └────┘ └───────┘
par └──────────┘ └────┘ └───────┘
pid └────┘ ┴ └───────┘
st ───┘└──────────┘└────────────────┘└─
45 have this : corec parallel.aux1 (l, S) = return a,
id └───┘ └───────────┘ ┴┴ ┴ └────┘ ┴
src └──────────┘└───┘┴└───────────┘┴┴ └┘ └┘ ┴└────┘┴
typ └──────────┘└───┘┴└───────────┘┴┴┴└┘┴└┘ ┴└────┘┴┴
doc └──────────┘└───┘┴ ┴ └┘ └┘ ┴└────┘┴
txt └──────────┘ ┴ ┴ └┘ └┘ ┴ ┴
par └──────────┘ ┴ ┴ └┘ └┘ ┴ ┴
pid └───────┘└─┘ ┴ ┴ └┘ └┘ ┴ ┴
st ────────────────────────────────────────────────────┘└─
46 { apply destruct_eq_ret, simp [parallel.aux1], rw e, simp [rmap] },
id └─────────────┘ └───────────┘ ┴ └──┘
src └────┘└─────────────┘ └────┘└───────────┘┴ └─┘ └────┘└──┘└┘
typ └────┘└─────────────┘ └────┘└───────────┘┴ └─┘┴ └────┘└──┘└┘
doc └────┘ └────┘ ┴ └─┘ └────┘└──┘└┘
txt └────┘ └────┘ ┴ └─┘ └────┘ └┘
par └────┘ └────┘ ┴ └─┘ └────┘ └┘
pid ┴ ┴┴ ┴ ┴ ┴┴ ┴┴
st ─────┘└───────────────────┘└────────────────────┘└────┘└────────────┘└┘└
47 rw this, apply_instance },
id └──┘
src └─┘ └─────────────┘
typ └─┘└──┘ └─────────────┘
doc └─┘ └─────────────┘
txt └─┘ └─────────────┘
par └─┘ └─────────────┘
pid ┴ ┴
st ──────────┘└───────────────┘└┘└
48 intros l S c m T, revert l S,
src └──────────────┘ └────────┘
typ └──────────────┘ └────────┘
doc └──────────────┘ └────────┘
txt └──────────────┘ └────────┘
par └──────────────┘ └────────┘
pid └────────┘ └──┘
st ─────────────────┘└──────────┘└─
49 apply @terminates_rec_on _ _ c T _ _,
id └───────────────┘ ┴ ┴
src └────┘ └───────────────┘└───┘ ┴ └──┘
typ └────┘ └───────────────┘└───┘┴┴┴└──┘
doc └────┘ └───┘ ┴ └──┘
txt └────┘ └───┘ ┴ └──┘
par └────┘ └───┘ ┴ └──┘
pid ┴ └───┘ ┴ └──┘
st ─────────────────────────────────────┘└─
50 { intros a l S m, apply lem1,
src └────────────┘ └────┘
typ └────────────┘ └────┘
doc └────────────┘ └────┘
txt └────────────┘ └────┘
par └────────────┘ └────┘
pid └──────┘ ┴
st ───┘└────────────┘└──────────┘└─
51 induction l with c l IH generalizing m; simp at m, { contradiction },
id ┴
src └────────┘ └─────────────────────────┘ └───────┘ └────────────┘
typ └────────┘┴└─────────────────────────┘ └───────┘ └────────────┘
doc └────────┘ └─────────────────────────┘ └───────┘ └────────────┘
txt └────────┘ └─────────────────────────┘ └───────┘ └────────────┘
par └────────┘ └─────────────────────────┘ └───────┘ └────────────┘
pid ┴ ┴└─────────┘└─────────────┘ ┴└──┘ ┴
st ────────────────────────────────────────────────────┘└──┘└────────────┘└┘└
52 cases m with e m,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ───────────────────┘└─
53 { rw ←e, simp [parallel.aux2],
id ┴ └───────────┘
src └──┘ └────┘└───────────┘┴
typ └──┘┴ └────┘└───────────┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid └┘ ┴┴ ┴
st ─────┘└───┘└────────────────────┘└─
54 cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls,
id └────────┘ └────────────────────┘ └─────┘ └──────┘ ┴
src └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘ └─────────┘
typ └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘┴└─────────┘
doc └────┘ ┴ ┴ ┴ └┘ └─────────┘
txt └────┘ ┴ ┴ ┴ └┘ └─────────┘
par └────┘ ┴ ┴ ┴ └┘ └─────────┘
pid ┴ ┴ ┴ ┴ └┘ └─────────┘
st ────────────────────────────────────────────────────────────────────────────┘└─
55 exacts [⟨a', rfl⟩, ⟨a, rfl⟩] },
id └┘ └─┘ ┴ └─┘
src └──────┘ └┘└─┘└─┘ └┘└─┘└─┘
typ └──────┘ └┘└┘└─┘└─┘ ┴└┘└─┘└─┘
doc └──────┘ └┘ └─┘ └┘ └─┘
txt └──────┘ └┘ └─┘ └┘ └─┘
par └──────┘ └┘ └─┘ └┘ └─┘
pid └┘ └┘ └─┘ └┘ └┘┴
st ──────────────────────────────────┘└┘└
56 { cases IH m with a' e,
id └┘ ┴
src └────┘ ┴ └────────┘
typ └────┘└┘┴┴└────────┘
doc └────┘ ┴ └────────┘
txt └────┘ ┴ └────────┘
par └────┘ ┴ └────────┘
pid ┴ ┴ └────────┘
st ─────────────────────────┘└─
57 simp [parallel.aux2], simp [parallel.aux2] at e,
id └───────────┘ └───────────┘
src └────┘└───────────┘┴ └────┘└───────────┘└────┘
typ └────┘└───────────┘┴ └────┘└───────────┘└────┘
doc └────┘ ┴ └────┘ └────┘
txt └────┘ ┴ └────┘ └────┘
par └────┘ ┴ └────┘ └────┘
pid ┴┴ ┴ ┴┴ ┴┴└──┘
st ─────────────────────────┘└─────────────────────────┘└─
58 rw e, exact ⟨a', rfl⟩ } },
id ┴ └┘ └─┘
src └─┘ └────┘ └┘└─┘└┘
typ └─┘┴ └────┘ └┘└┘└─┘└┘
doc └─┘ └────┘ └┘ └┘
txt └─┘ └────┘ └┘ └┘
par └─┘ └────┘ └┘ └┘
pid ┴ ┴ └┘ ┴┴
st ─────────┘└────────────────┘└──┘└
59 { intros s IH l S m,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ────────────────────┘└─
60 have H1 : ∀ l', parallel.aux2 l = sum.inr l' → s ∈ l',
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴
src └────────┘ └─┘ ┴└───────────┘┴ ┴ ┴└─────┘┴ ┴ ┴ ┴┴┴
typ └────────┘ └─┘ ┴└───────────┘┴┴┴┴┴└─────┘┴ ┴ ┴┴┴┴┴
doc └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
61 { induction l with c l IH' generalizing m;
id ┴
src └────────┘ └──────────────────────────┘
typ └────────┘┴└──────────────────────────┘
doc └────────┘ └──────────────────────────┘
txt └────────┘ └──────────────────────────┘
par └────────┘ └──────────────────────────┘
pid ┴ ┴└──────────┘└─────────────┘
st ─────┘└────────────────────────────────────────
62 intros l' e'; simp at m, { contradiction },
src └──────────┘ └───────┘ └────────────┘
typ └──────────┘ └───────┘ └────────────┘
doc └──────────┘ └───────┘ └────────────┘
txt └──────────┘ └───────┘ └────────────┘
par └──────────┘ └───────┘ └────────────┘
pid └────┘ ┴└──┘ ┴
st ────────────────────────────┘└──┘└────────────┘└┘└
63 cases m with e m; simp [parallel.aux2] at e',
id ┴ └───────────┘
src └────┘ └───────┘ └────┘└───────────┘└─────┘
typ └────┘┴└───────┘ └────┘└───────────┘└─────┘
doc └────┘ └───────┘ └────┘ └─────┘
txt └────┘ └───────┘ └────┘ └─────┘
par └────┘ └───────┘ └────┘ └─────┘
pid ┴ └───────┘ ┴┴ ┴┴└───┘
st ─────────────────────────────────────────────────┘└─
64 { rw ←e at e',
id ┴
src └──┘ └────┘
typ └──┘┴└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid └┘ └────┘
st ───────┘└─────────┘└─
65 cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls;
id └────────┘ └────────────────────┘ └─────┘ └──────┘ ┴
src └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘ └─────────┘
typ └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘┴└─────────┘
doc └────┘ ┴ ┴ ┴ └┘ └─────────┘
txt └────┘ ┴ ┴ ┴ └┘ └─────────┘
par └────┘ ┴ ┴ ┴ └┘ └─────────┘
pid ┴ ┴ ┴ ┴ └┘ └─────────┘
st ─────────────────────────────────────────────────────────────────────────────────
66 injection e' with e', rw ←e', simp },
id └┘ └┘
src └────────┘ └──────┘ └──┘ └───┘
typ └────────┘└┘└──────┘ └──┘└┘ └───┘
doc └────────┘ └──────┘ └──┘ └───┘
txt └────────┘ └──────┘ └──┘ └───┘
par └────────┘ └──────┘ └──┘ └───┘
pid ┴ └──────┘ └┘ ┴
st ───────────────────────────┘└──────┘└─────┘└┘└
67 { induction e : list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a' ls;
id └────────┘ └────────────────────┘ └─────┘ └──────┘ ┴
src └────────┘ └─┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘ └─────────┘
typ └────────┘ └─┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘┴└─────────┘
doc └────────┘ └─┘ ┴ ┴ ┴ └┘ └─────────┘
txt └────────┘ └─┘ ┴ ┴ ┴ └┘ └─────────┘
par └────────┘ └─┘ ┴ ┴ ┴ └┘ └─────────┘
pid ┴ └─┘ ┴ ┴ ┴ └┘ ┴└────────┘
st ─────────────────────────────────────────────────────────────────────────────────────────
68 rw e at e', { contradiction },
id ┴
src └─┘ └────┘ └────────────┘
typ └─┘┴└────┘ └────────────┘
doc └─┘ └────┘ └────────────┘
txt └─┘ └────┘ └────────────┘
par └─┘ └────┘ └────────────┘
pid ┴ └────┘ ┴
st ──────────┘┴└────┘└──┘└────────────┘└┘└
69 have := IH' m _ e,
id └─┘ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘└─┘┴┴└─┘┴
doc └──────┘ ┴ └─┘
txt └──────┘ ┴ └─┘
par └──────┘ ┴ └─┘
pid └───┘└─┘ ┴ └─┘
st ────────────────────────┘└─
70 simp [parallel.aux2] at e',
id └───────────┘
src └────┘└───────────┘└─────┘
typ └────┘└───────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ─────────────────────────────────┘└─
71 cases destruct c; injection e' with h',
id └──────┘ ┴ └┘
src └────┘└──────┘┴ └────────┘ └──────┘
typ └────┘└──────┘┴┴ └────────┘└┘└──────┘
doc └────┘└──────┘┴ └────────┘ └──────┘
txt └────┘ ┴ └────────┘ └──────┘
par └────┘ ┴ └────────┘ └──────┘
pid ┴ ┴ ┴ └──────┘
st ─────────────────────────────────────────────┘└─
72 rw ←h', simp [this] } },
id └┘ └──┘
src └──┘ └────┘ └┘
typ └──┘└┘ └────┘└──┘└┘
doc └──┘ └────┘ └┘
txt └──┘ └────┘ └┘
par └──┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st ─────────────┘└────────────┘└──┘└
73 induction h : parallel.aux2 l with a l',
id └───────────┘ ┴
src └────────┘ └─┘└───────────┘┴ └────────┘
typ └────────┘ └─┘└───────────┘┴┴└────────┘
doc └────────┘ └─┘ ┴ └────────┘
txt └────────┘ └─┘ ┴ └────────┘
par └────────┘ └─┘ ┴ └────────┘
pid ┴ └─┘ ┴ ┴└───────┘
st ──────────────────────────────────────────┘└─
74 { exact lem1 _ _ ⟨a, h⟩ },
id └──┘ ┴ ┴
src └────┘ └───┘ └┘ └┘
typ └────┘└──┘└───┘ ┴└┘┴└┘
doc └────┘ └───┘ └┘ └┘
txt └────┘ └───┘ └┘ └┘
par └────┘ └───┘ └┘ └┘
pid ┴ └───┘ └┘ ┴┴
st ─────┘└────────────────────┘└┘└
75 { have H2 : corec parallel.aux1 (l, S) = think _,
id └───┘ └───────────┘ ┴┴ ┴ └───┘
src └────────┘└───┘┴└───────────┘┴┴ └┘ └┘ ┴└───┘└┘
typ └────────┘└───┘┴└───────────┘┴┴┴└┘┴└┘ ┴└───┘└┘
doc └────────┘└───┘┴ ┴ └┘ └┘ ┴└───┘└┘
txt └────────┘ ┴ ┴ └┘ └┘ ┴ └┘
par └────────┘ ┴ ┴ └┘ └┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴ └┘ └┘ ┴ └┘
st ───────────────────────────────────────────────────┘└─
76 { apply destruct_eq_think,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────┘└─────────────────────┘└─
77 simp [parallel.aux1],
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────────────────────────┘└─
78 rw h, simp [rmap] },
id ┴ └──┘
src └─┘ └────┘└──┘└┘
typ └─┘┴ └────┘└──┘└┘
doc └─┘ └────┘└──┘└┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ───────────┘└────────────┘└┘└
79 rw H2, apply @computation.think_terminates _ _ _,
id └┘ └──────────────────────────┘
src └─┘ └────┘ └──────────────────────────┘└────┘
typ └─┘└┘ └────┘ └──────────────────────────┘└────┘
doc └─┘ └────┘ └────┘
txt └─┘ └────┘ └────┘
par └─┘ └────┘ └────┘
pid ┴ ┴ └────┘
st ──────────┘└─────────────────────────────────────────┘└─
80 have := H1 _ h,
id └┘ ┴
src └──────┘ └─┘
typ └──────┘└┘└─┘┴
doc └──────┘ └─┘
txt └──────┘ └─┘
par └──────┘ └─┘
pid └───┘└─┘ └─┘
st ───────────────────┘└─
81 rcases seq.destruct S with _ | ⟨_|c, S'⟩;
id └──────────┘ ┴
src └─────┘└──────────┘┴ └─────────────────┘
typ └─────┘└──────────┘┴┴└─────────────────┘
doc └─────┘└──────────┘┴ └─────────────────┘
txt └─────┘ ┴ └─────────────────┘
par └─────┘ ┴ └─────────────────┘
pid ┴ ┴ └─────────────────┘
st ────────────────────────────────────────────────
82 simp [parallel.aux1]; apply IH; simp [this] } }
id └───────────┘ └──┘
src └────┘└───────────┘┴ └────┘ └────┘ └┘
typ └────┘└───────────┘┴ └────┘ └────┘└──┘└┘
doc └────┘ ┴ └────┘ └────┘ └┘
txt └────┘ ┴ └────┘ └────┘ └┘
par └────┘ ┴ └────┘ └────┘ └┘
pid ┴┴ ┴ ┴ ┴┴ ┴┴
st ─────────────────────────────────────────────────┘└───
83 end
st ──┘
84
85 theorem terminates_parallel {S : wseq (computation α)}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
86 {c} (h : c ∈ S) [T : terminates c] : terminates (parallel S) :=
id ┴ ┴ ┴ └────────┘ ┴ └────────┘ └──────┘ ┴
src ┴ └────────┘ └────────┘ └──────┘
typ ┴ ┴ ┴ └────────┘ ┴ └────────┘ └──────┘ ┴
doc └────────┘ └────────┘ └──────┘
87 suffices ∀ n (l : list (computation α)) S c,
id ┴ └──┘ └─────────┘ ┴ ┴ ┴
src └──┘ └─────────┘
typ ┴ └──┘ └─────────┘ ┴ ┴ ┴
doc └─────────┘
88 c ∈ l ∨ some (some c) = seq.nth S n →
id ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └─────┘ ┴ ┴
src ┴ ┴ └──┘ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
89 terminates c → terminates (corec parallel.aux1 (l, S)),
id └────────┘ ┴ └────────┘ └───┘ └───────────┘ ┴┴ ┴
src └────────┘ └────────┘ └───┘ └───────────┘ ┴
typ └────────┘ ┴ └────────┘ └───┘ └───────────┘ ┴┴ ┴
doc └────────┘ └────────┘ └───┘
90 from let ⟨n, h⟩ := h in this n [] S c (or.inr h) T,
id └─┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └────┘ ┴
src └┘ └────┘
typ └─┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └────┘ ┴
91 begin
st └─────
92 intro n, induction n with n IH; intros l S c o T,
id ┴
src └─────┘ └────────┘ └────────┘ └──────────────┘
typ └─────┘ └────────┘┴└────────┘ └──────────────┘
doc └─────┘ └────────┘ └────────┘ └──────────────┘
txt └─────┘ └────────┘ └────────┘ └──────────────┘
par └─────┘ └────────┘ └────────┘ └──────────────┘
pid └┘ ┴ ┴└───────┘ └────────┘
st ────────┘└───────────────────────────────────────┘└─
93 { cases o with a a, { exact terminates_parallel.aux a T },
id ┴ └─────────────────────┘ ┴ ┴
src └────┘ └───────┘ └────┘└─────────────────────┘┴ ┴ ┴
typ └────┘┴└───────┘ └────┘└─────────────────────┘┴┴┴┴┴
doc └────┘ └───────┘ └────┘ ┴ ┴ ┴
txt └────┘ └───────┘ └────┘ ┴ ┴ ┴
par └────┘ └───────┘ └────┘ ┴ ┴ ┴
pid ┴ └───────┘ ┴ ┴ ┴ ┴
st ───┘└──────────────┘└──┘└────────────────────────────────┘└┘└
94 have H : seq.destruct S = some (some c, _),
id └──────────┘ ┴ ┴ ┴└──┘ ┴
src └───────┘└──────────┘┴ ┴┴┴ ┴┴└──┘┴ └──┘
typ └───────┘└──────────┘┴┴┴┴┴ ┴┴└──┘┴┴└──┘
doc └───────┘└──────────┘┴ ┴ ┴ ┴ ┴ └──┘
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘
st ─────────────────────────────────────────────┘└─
95 { unfold seq.destruct functor.map, rw ← a, simp },
id ┴
src └─────────────────────────────┘ └───┘ └───┘
typ └─────────────────────────────┘ └───┘┴ └───┘
doc └─────────────────────────────┘ └───┘ └───┘
txt └─────────────────────────────┘ └───┘ └───┘
par └─────────────────────────────┘ └───┘ └───┘
pid └───────────────────────┘ └─┘ ┴
st ─────┘└─────────────────────────────┘└──────┘└─────┘└┘└
96 induction h : parallel.aux2 l with a l';
id └───────────┘ ┴
src └────────┘ └─┘└───────────┘┴ └────────┘
typ └────────┘ └─┘└───────────┘┴┴└────────┘
doc └────────┘ └─┘ ┴ └────────┘
txt └────────┘ └─┘ ┴ └────────┘
par └────────┘ └─┘ ┴ └────────┘
pid ┴ └─┘ ┴ ┴└───────┘
st ─────────────────────────────────────────────
97 have C : corec parallel.aux1 (l, S) = _,
id └───┘ └───────────┘ ┴┴ ┴
src └───────┘└───┘┴└───────────┘┴┴ └┘ └┘ └┘
typ └───────┘└───┘┴└───────────┘┴┴┴└┘┴└┘ └┘
doc └───────┘└───┘┴ ┴ └┘ └┘ └┘
txt └───────┘ ┴ ┴ └┘ └┘ └┘
par └───────┘ ┴ ┴ └┘ └┘ └┘
pid └────┘└─┘ ┴ ┴ └┘ └┘ └┘
st ──────────────────────────────────────────┘└─
98 { apply destruct_eq_ret, simp [parallel.aux1], rw [h], simp [rmap] },
id └─────────────┘ └───────────┘ ┴ └──┘
src └────┘└─────────────┘ └────┘└───────────┘┴ └──┘ ┴ └────┘└──┘└┘
typ └────┘└─────────────┘ └────┘└───────────┘┴ └──┘┴┴ └────┘└──┘└┘
doc └────┘ └────┘ ┴ └──┘ ┴ └────┘└──┘└┘
txt └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
par └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
pid ┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴┴
st ─────┘└───────────────────┘└────────────────────┘└─────┘└─────────────┘└┘└
99 { rw C, resetI, apply_instance },
id ┴
src └─┘ └────┘ └─────────────┘
typ └─┘┴ └────┘ └─────────────┘
doc └─┘ └────┘ └─────────────┘
txt └─┘ └────┘ └─────────────┘
par └─┘ └────┘ └─────────────┘
pid ┴ ┴
st ─────┘└──┘└───────────────────────┘└┘└
100 { apply destruct_eq_think, simp [parallel.aux1], rw [h, H], simp [rmap] },
id └───────────────┘ └───────────┘ ┴ ┴ └──┘
src └────┘└───────────────┘ └────┘└───────────┘┴ └──┘ └┘ ┴ └────┘└──┘└┘
typ └────┘└───────────────┘ └────┘└───────────┘┴ └──┘┴└┘┴┴ └────┘└──┘└┘
doc └────┘ └────┘ ┴ └──┘ └┘ ┴ └────┘└──┘└┘
txt └────┘ └────┘ ┴ └──┘ └┘ ┴ └────┘ └┘
par └────┘ └────┘ ┴ └──┘ └┘ ┴ └────┘ └┘
pid ┴ ┴┴ ┴ └┘ └┘ ┴ ┴┴ ┴┴
st ─────┘└─────────────────────┘└────────────────────┘└─────┘└─┘└─────────────┘└┘└
101 { rw C, apply @computation.think_terminates _ _ _,
id ┴ └──────────────────────────┘
src └─┘ └────┘ └──────────────────────────┘└────┘
typ └─┘┴ └────┘ └──────────────────────────┘└────┘
doc └─┘ └────┘ └────┘
txt └─┘ └────┘ └────┘
par └─┘ └────┘ └────┘
pid ┴ ┴ └────┘
st ─────────┘└─────────────────────────────────────────┘└─
102 apply terminates_parallel.aux _ T, simp } },
id └─────────────────────┘ ┴
src └────┘└─────────────────────┘└─┘ └───┘
typ └────┘└─────────────────────┘└─┘┴ └───┘
doc └────┘ └─┘ └───┘
txt └────┘ └─┘ └───┘
par └────┘ └─┘ └───┘
pid ┴ └─┘ ┴
st ──────────────────────────────────────┘└─────┘└──┘└
103 { cases o with a a, { exact terminates_parallel.aux a T },
id ┴ └─────────────────────┘ ┴ ┴
src └────┘ └───────┘ └────┘└─────────────────────┘┴ ┴ ┴
typ └────┘┴└───────┘ └────┘└─────────────────────┘┴┴┴┴┴
doc └────┘ └───────┘ └────┘ ┴ ┴ ┴
txt └────┘ └───────┘ └────┘ ┴ ┴ ┴
par └────┘ └───────┘ └────┘ ┴ ┴ ┴
pid ┴ └───────┘ ┴ ┴ ┴ ┴
st ───────────────────┘└──┘└────────────────────────────────┘└┘└
104 induction h : parallel.aux2 l with a l';
id └───────────┘ ┴
src └────────┘ └─┘└───────────┘┴ └────────┘
typ └────────┘ └─┘└───────────┘┴┴└────────┘
doc └────────┘ └─┘ ┴ └────────┘
txt └────────┘ └─┘ ┴ └────────┘
par └────────┘ └─┘ ┴ └────────┘
pid ┴ └─┘ ┴ ┴└───────┘
st ─────────────────────────────────────────────
105 have C : corec parallel.aux1 (l, S) = _,
id └───┘ └───────────┘ ┴┴ ┴
src └───────┘└───┘┴└───────────┘┴┴ └┘ └┘ └┘
typ └───────┘└───┘┴└───────────┘┴┴┴└┘┴└┘ └┘
doc └───────┘└───┘┴ ┴ └┘ └┘ └┘
txt └───────┘ ┴ ┴ └┘ └┘ └┘
par └───────┘ ┴ ┴ └┘ └┘ └┘
pid └────┘└─┘ ┴ ┴ └┘ └┘ └┘
st ──────────────────────────────────────────┘└─
106 { apply destruct_eq_ret, simp [parallel.aux1], rw [h], simp [rmap] },
id └─────────────┘ └───────────┘ ┴ └──┘
src └────┘└─────────────┘ └────┘└───────────┘┴ └──┘ ┴ └────┘└──┘└┘
typ └────┘└─────────────┘ └────┘└───────────┘┴ └──┘┴┴ └────┘└──┘└┘
doc └────┘ └────┘ ┴ └──┘ ┴ └────┘└──┘└┘
txt └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
par └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
pid ┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴┴
st ─────┘└───────────────────┘└────────────────────┘└─────┘└─────────────┘└┘└
107 { rw C, resetI, apply_instance },
id ┴
src └─┘ └────┘ └─────────────┘
typ └─┘┴ └────┘ └─────────────┘
doc └─┘ └────┘ └─────────────┘
txt └─┘ └────┘ └─────────────┘
par └─┘ └────┘ └─────────────┘
pid ┴ ┴
st ─────┘└──┘└───────────────────────┘└┘└
108 { apply destruct_eq_think, simp [parallel.aux1], rw [h], simp [rmap] },
id └───────────────┘ └───────────┘ ┴ └──┘
src └────┘└───────────────┘ └────┘└───────────┘┴ └──┘ ┴ └────┘└──┘└┘
typ └────┘└───────────────┘ └────┘└───────────┘┴ └──┘┴┴ └────┘└──┘└┘
doc └────┘ └────┘ ┴ └──┘ ┴ └────┘└──┘└┘
txt └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
par └────┘ └────┘ ┴ └──┘ ┴ └────┘ └┘
pid ┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴┴
st ─────┘└─────────────────────┘└────────────────────┘└─────┘└─────────────┘└┘└
109 { rw C, apply @computation.think_terminates _ _ _,
id ┴ └──────────────────────────┘
src └─┘ └────┘ └──────────────────────────┘└────┘
typ └─┘┴ └────┘ └──────────────────────────┘└────┘
doc └─┘ └────┘ └────┘
txt └─┘ └────┘ └────┘
par └─┘ └────┘ └────┘
pid ┴ ┴ └────┘
st ─────────┘└─────────────────────────────────────────┘└─
110 have TT : ∀ l', terminates (corec parallel.aux1 (l', S.tail)),
id └────────┘ └───┘ └───────────┘ ┴ └────┘
src └────────┘ └─┘ ┴└────────┘┴ └───┘┴└───────────┘┴┴ └┘└────┘└┘
typ └────────┘ └─┘ ┴└────────┘┴ └───┘┴└───────────┘┴┴ └┘└────┘└┘
doc └────────┘ └─┘ ┴└────────┘┴ └───┘┴ ┴ └┘└────┘└┘
txt └────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
par └────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ ┴ └┘ └┘
st ──────────────────────────────────────────────────────────────────┘└─
111 { intro, apply IH _ _ _ (or.inr _) T, rw a, cases S with f al, refl },
id └┘ └────┘ ┴ ┴ ┴
src └───┘ └────┘ └─────┘ └────┘└──┘ └─┘ └────┘ └────────┘ └───┘
typ └───┘ └────┘└┘└─────┘ └────┘└──┘┴ └─┘┴ └────┘┴└────────┘ └───┘
doc └───┘ └────┘ └─────┘ └──┘ └─┘ └────┘ └────────┘ └───┘
txt └───┘ └────┘ └─────┘ └──┘ └─┘ └────┘ └────────┘ └───┘
par └───┘ └────┘ └─────┘ └──┘ └─┘ └────┘ └────────┘ └───┘
pid ┴ └─────┘ └──┘ ┴ ┴ └────────┘ ┴
st ───────┘└───┘└───────────────────────────┘└────┘└─────────────────┘└─────┘└┘└
112 induction e : seq.nth S 0 with o,
id └─────┘ ┴
src └────────┘ └─┘└─────┘┴ └───────┘
typ └────────┘ └─┘└─────┘┴┴└───────┘
doc └────────┘ └─┘└─────┘┴ └───────┘
txt └────────┘ └─┘ ┴ └───────┘
par └────────┘ └─┘ ┴ └───────┘
pid ┴ └─┘ ┴ ┴└┘└────┘
st ─────────────────────────────────────┘└─
113 { have D : seq.destruct S = none,
id └──────────┘ ┴ └──┘
src └───────┘└──────────┘┴ ┴ ┴└──┘
typ └───────┘└──────────┘┴┴┴ ┴└──┘
doc └───────┘└──────────┘┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴
pid └────┘└─┘ ┴ ┴ ┴
st ───────┘└────────────────────────────┘└─
114 { dsimp [seq.destruct], rw e, refl },
id └──────────┘ ┴
src └─────┘└──────────┘┴ └─┘ └───┘
typ └─────┘└──────────┘┴ └─┘┴ └───┘
doc └─────┘└──────────┘┴ └─┘ └───┘
txt └─────┘ ┴ └─┘ └───┘
par └─────┘ ┴ └─┘ └───┘
pid ┴┴ ┴ ┴ ┴
st ─────────┘└──────────────────┘└────┘└─────┘└┘└
115 rw D, simp [parallel.aux1], have TT := TT l',
id ┴ └───────────┘ └┘ └┘
src └─┘ └────┘└───────────┘┴ └─────────┘ ┴
typ └─┘┴ └────┘└───────────┘┴ └─────────┘└┘┴└┘
doc └─┘ └────┘ ┴ └─────────┘ ┴
txt └─┘ └────┘ ┴ └─────────┘ ┴
par └─┘ └────┘ ┴ └─────────┘ ┴
pid ┴ ┴┴ ┴ └─────┘┴└─┘ ┴
st ───────────┘└────────────────────┘└────────────────┘└─
116 rwa [seq.destruct_eq_nil D, seq.tail_nil] at TT },
id └─────────────────┘ ┴ └──────────┘
src └───┘└─────────────────┘┴ └┘└──────────┘└──────┘
typ └───┘└─────────────────┘┴┴└┘└──────────┘└──────┘
doc └───┘ ┴ └┘ └──────┘
txt └───┘ ┴ └┘ └──────┘
par └───┘ ┴ └┘ └──────┘
pid └┘ ┴ └┘ ┴└────┘┴
st ─────────────────────────────────┘└────────────┘┴└─────┘└┘└
117 { have D : seq.destruct S = some (o, S.tail),
id └──────────┘ └──┘ ┴┴ └────┘
src └───────┘└──────────┘┴ ┴ ┴└──┘┴┴ └┘└────┘┴
typ └───────┘└──────────┘┴ ┴ ┴└──┘┴┴┴└┘└────┘┴
doc └───────┘└──────────┘┴ ┴ ┴ ┴ └┘└────┘┴
txt └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────┘└─
118 { dsimp [seq.destruct], rw e, refl },
id └──────────┘ ┴
src └─────┘└──────────┘┴ └─┘ └───┘
typ └─────┘└──────────┘┴ └─┘┴ └───┘
doc └─────┘└──────────┘┴ └─┘ └───┘
txt └─────┘ ┴ └─┘ └───┘
par └─────┘ ┴ └─┘ └───┘
pid ┴┴ ┴ ┴ ┴
st ─────────┘└──────────────────┘└────┘└─────┘└┘└
119 rw D, cases o with c; simp [parallel.aux1, TT] } } }
id ┴ ┴ └───────────┘ └┘
src └─┘ └────┘ └─────┘ └────┘└───────────┘└┘ └┘
typ └─┘┴ └────┘┴└─────┘ └────┘└───────────┘└┘└┘└┘
doc └─┘ └────┘ └─────┘ └────┘ └┘ └┘
txt └─┘ └────┘ └─────┘ └────┘ └┘ └┘
par └─┘ └────┘ └─────┘ └────┘ └┘ └┘
pid ┴ ┴ └─────┘ ┴┴ └┘ ┴┴
st ───────────┘└─────────────────────────────────────────┘└─────
120 end
st ──┘
121
122 theorem exists_of_mem_parallel {S : wseq (computation α)}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
123 {a} (h : a ∈ parallel S) : ∃ c ∈ S, a ∈ c :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──────┘
124 suffices ∀ C, a ∈ C → ∀ (l : list (computation α)) S,
id ┴ ┴ ┴ ┴ └──┘ └─────────┘ ┴ ┴
src ┴ └──┘ └─────────┘
typ ┴ ┴ ┴ ┴ └──┘ └─────────┘ ┴ ┴
doc └─────────┘
125 corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c,
id └───┘ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ └───────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
126 from let ⟨c, h1, h2⟩ := this _ h [] S rfl in ⟨c, h1.resolve_left id, h2⟩,
id └─┘ ┴ └┘ └┘ └──┘ ┴ └┘ ┴ └─┘ └───────────┘ └┘
src └┘ └─┘ └───────────┘ └┘
typ └─┘ ┴ └┘ └┘ └──┘ ┴ └┘ ┴ └─┘ └───────────┘ └┘
127 begin
st └─────
128 let F : list (computation α) → α ⊕ list (computation α) → Prop,
id └──┘ ┴ └──┘ └─────────┘ ┴
src └──────┘ ┴ ┴ └┘ ┴ ┴┴┴└──┘┴ └─────────┘┴ └┘ ┴
typ └──────┘└──┘┴ ┴ └┘ ┴ ┴┴┴└──┘┴ └─────────┘┴┴└┘ ┴
doc └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────┘┴ └┘ ┴
txt └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
129 { intros l a, cases a with a l',
id ┴
src └────────┘ └────┘ └────────┘
typ └────────┘ └────┘┴└────────┘
doc └────────┘ └────┘ └────────┘
txt └────────┘ └────┘ └────────┘
par └────────┘ └────┘ └────────┘
pid └──┘ ┴ └────────┘
st ───┘└────────┘└─────────────────┘└─
130 exact ∃ c ∈ l, a ∈ c,
id ┴ ┴┴ ┴
src └────┘┴└───┘ ┴┴ ┴ ┴
typ └────┘┴└───┘┴┴┴┴┴ ┴
doc └────┘ └───┘ ┴ ┴ ┴
txt └────┘ └───┘ ┴ ┴ ┴
par └────┘ └───┘ ┴ ┴ ┴
pid ┴ └───┘ ┴ ┴ ┴
st ───────────────────────┘└─
131 exact ∀ a', (∃ c ∈ l', a' ∈ c) → (∃ c ∈ l, a' ∈ c) },
id ┴ └┘┴ ┴
src └────┘ └─┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘
typ └────┘ └─┘ ┴ ┴└───┘└┘┴┴ ┴ ┴ └┘ ┴ └───┘┴ ┴ ┴ ┴ └┘
doc └────┘ └─┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘
txt └────┘ └─┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘
par └────┘ └─┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘
pid ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────┘└┘└
132 have lem1 : ∀ (l : list (computation α)), F l (parallel.aux2 l),
id └──┘ └─────────┘ ┴ ┴ └───────────┘
src └──────────┘ └────┘└──┘┴ └─────────┘┴ └┘ ┴ ┴ ┴ └───────────┘┴ ┴
typ └──────────┘ └────┘└──┘┴ └─────────┘┴┴└┘ ┴┴┴ ┴ └───────────┘┴ ┴
doc └──────────┘ └────┘ ┴ └─────────┘┴ └┘ ┴ ┴ ┴ ┴ ┴
txt └──────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid └───────┘└─┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────┘└─
133 { intro l, induction l with c l IH; simp [parallel.aux2],
id ┴ └───────────┘
src └─────┘ └────────┘ └──────────┘ └────┘└───────────┘┴
typ └─────┘ └────────┘┴└──────────┘ └────┘└───────────┘┴
doc └─────┘ └────────┘ └──────────┘ └────┘ ┴
txt └─────┘ └────────┘ └──────────┘ └────┘ ┴
par └─────┘ └────────┘ └──────────┘ └────┘ ┴
pid └┘ ┴ ┴└─────────┘ ┴┴ ┴
st ───┘└─────┘└─────────────────────────────────────────────┘└─
134 { intros a h, rcases h with ⟨c, hn, _⟩,
id ┴
src └────────┘ └─────┘ └──────────────┘
typ └────────┘ └─────┘┴└──────────────┘
doc └────────┘ └─────┘ └──────────────┘
txt └────────┘ └─────┘ └──────────────┘
par └────────┘ └─────┘ └──────────────┘
pid └──┘ ┴ └──────────────┘
st ─────┘└────────┘└────────────────────────┘└─
135 exact false.elim hn },
id └────────┘ └┘
src └────┘└────────┘┴ ┴
typ └────┘└────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────┘└┘└
136 { simp [parallel.aux2] at IH,
id └───────────┘
src └────┘└───────────┘└─────┘
typ └────┘└───────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ───────────────────────────────┘└─
137 cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l with a ls;
id └────────┘ └────────────────────┘ └─────┘ └──────┘ ┴
src └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘ └────────┘
typ └────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘┴└────────┘
doc └────┘ ┴ ┴ ┴ └┘ └────────┘
txt └────┘ ┴ ┴ ┴ └┘ └────────┘
par └────┘ ┴ ┴ ┴ └┘ └────────┘
pid ┴ ┴ ┴ ┴ └┘ └────────┘
st ──────────────────────────────────────────────────────────────────────────────
138 simp [parallel.aux2],
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────────────┘└─
139 { rcases IH with ⟨c', cl, ac⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ───────┘└─────────────────────────┘└─
140 refine ⟨c', or.inr cl, ac⟩ },
id └┘ └────┘ └┘ └┘
src └─────┘ └┘└────┘┴ └┘ └┘
typ └─────┘ └┘└┘└────┘┴└┘└┘└┘└┘
doc └─────┘ └┘ ┴ └┘ └┘
txt └─────┘ └┘ ┴ └┘ └┘
par └─────┘ └┘ ┴ └┘ └┘
pid ┴ └┘ ┴ └┘ ┴┴
st ──────────────────────────────────┘└┘└
141 { induction h : destruct c with a c'; simp [rmap],
id └──────┘ ┴ └──┘
src └────────┘ └─┘└──────┘┴ └────────┘ └────┘└──┘┴
typ └────────┘ └─┘└──────┘┴┴└────────┘ └────┘└──┘┴
doc └────────┘ └─┘└──────┘┴ └────────┘ └────┘└──┘┴
txt └────────┘ └─┘ ┴ └────────┘ └────┘ ┴
par └────────┘ └─┘ ┴ └────────┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴└───────┘ ┴┴ ┴
st ──────────────────────────────────────────────────────┘└─
142 { refine ⟨c, list.mem_cons_self _ _, _⟩,
id ┴ └────────────────┘
src └─────┘ └┘└────────────────┘└──────┘
typ └─────┘ ┴└┘└────────────────┘└──────┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴ └┘ └──────┘
st ─────────┘└───────────────────────────────────┘└─
143 rw destruct_eq_ret h,
id └─────────────┘ ┴
src └─┘└─────────────┘┴
typ └─┘└─────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└─
144 apply ret_mem },
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────┘└┘└
145 { intros a' h, rcases h with ⟨d, dm, ad⟩,
id ┴
src └─────────┘ └─────┘ └───────────────┘
typ └─────────┘ └─────┘┴└───────────────┘
doc └─────────┘ └─────┘ └───────────────┘
txt └─────────┘ └─────┘ └───────────────┘
par └─────────┘ └─────┘ └───────────────┘
pid └───┘ ┴ └───────────────┘
st ────────────────────┘└─────────────────────────┘└─
146 simp at dm, cases dm with e dl,
id └┘
src └────────┘ └────┘ └────────┘
typ └────────┘ └────┘└┘└────────┘
doc └────────┘ └────┘ └────────┘
txt └────────┘ └────┘ └────────┘
par └────────┘ └────┘ └────────┘
pid ┴└───┘ ┴ └────────┘
st ───────────────────┘└──────────────────┘└─
147 { rw e at ad, refine ⟨c, list.mem_cons_self _ _, _⟩,
id ┴ ┴ └────────────────┘
src └─┘ └────┘ └─────┘ └┘└────────────────┘└──────┘
typ └─┘┴└────┘ └─────┘ ┴└┘└────────────────┘└──────┘
doc └─┘ └────┘ └─────┘ └┘ └──────┘
txt └─┘ └────┘ └─────┘ └┘ └──────┘
par └─┘ └────┘ └─────┘ └┘ └──────┘
pid ┴ └────┘ ┴ └┘ └──────┘
st ───────────┘└────────┘└─────────────────────────────────────┘└─
148 rw destruct_eq_think h,
id └───────────────┘ ┴
src └─┘└───────────────┘┴
typ └─┘└───────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────────────────────────────┘└─
149 exact think_mem ad },
id └───────┘ └┘
src └────┘└───────┘┴ ┴
typ └────┘└───────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────┘└┘└
150 { cases IH a' ⟨d, dl, ad⟩ with d dm, cases dm with dm ad,
id └┘ └┘ ┴ └┘ └┘ └┘
src └────┘ ┴ ┴ └┘ └┘ └─────────┘ └────┘ └─────────┘
typ └────┘└┘┴└┘┴ ┴└┘└┘└┘└┘└─────────┘ └────┘└┘└─────────┘
doc └────┘ ┴ ┴ └┘ └┘ └─────────┘ └────┘ └─────────┘
txt └────┘ ┴ ┴ └┘ └┘ └─────────┘ └────┘ └─────────┘
par └────┘ ┴ ┴ └┘ └┘ └─────────┘ └────┘ └─────────┘
pid ┴ ┴ ┴ └┘ └┘ ┴└────────┘ ┴ └─────────┘
st ────────────────────────────────────────────┘└───────────────────┘└─
151 exact ⟨d, or.inr dm, ad⟩ } } } } },
id ┴ └────┘ └┘ └┘
src └────┘ └┘└────┘┴ └┘ └┘
typ └────┘ ┴└┘└────┘┴└┘└┘└┘└┘
doc └────┘ └┘ ┴ └┘ └┘
txt └────┘ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ └┘
pid ┴ └┘ ┴ └┘ ┴┴
st ────────────────────────────────────┘└────────┘└
152 intros C aC, refine mem_rec_on aC _ (λ C' IH, _);
id └────────┘ └┘
src └─────────┘ └─────┘└────────┘┴ └─┘ └────────┘
typ └─────────┘ └─────┘└────────┘┴└┘└─┘ └────────┘
doc └─────────┘ └─────┘ ┴ └─┘ └────────┘
txt └─────────┘ └─────┘ ┴ └─┘ └────────┘
par └─────────┘ └─────┘ ┴ └─┘ └────────┘
pid └───┘ ┴ ┴ └─┘ └────────┘
st ────────────┘└──────────────────────────────────────
153 intros l S e; have e' := congr_arg destruct e; have := lem1 l;
id └───────┘ └──────┘ ┴ └──┘ ┴
src └──────────┘ └─────────┘└───────┘┴└──────┘┴ └──────┘ ┴
typ └──────────┘ └─────────┘└───────┘┴└──────┘┴┴ └──────┘└──┘┴┴
doc └──────────┘ └─────────┘ ┴└──────┘┴ └──────┘ ┴
txt └──────────┘ └─────────┘ ┴ ┴ └──────┘ ┴
par └──────────┘ └─────────┘ ┴ ┴ └──────┘ ┴
pid └────┘ └─────┘┴└─┘ ┴ ┴ └───┘└─┘ ┴
st ─────────────────────────────────────────────────────────────────
154 simp [parallel.aux1] at e'; cases parallel.aux2 l with a' l'; injection e' with h',
id └───────────┘ └───────────┘ ┴ └┘
src └────┘└───────────┘└─────┘ └────┘└───────────┘┴ └─────────┘ └────────┘ └──────┘
typ └────┘└───────────┘└─────┘ └────┘└───────────┘┴┴└─────────┘ └────────┘└┘└──────┘
doc └────┘ └─────┘ └────┘ ┴ └─────────┘ └────────┘ └──────┘
txt └────┘ └─────┘ └────┘ ┴ └─────────┘ └────────┘ └──────┘
par └────┘ └─────┘ └────┘ ┴ └─────────┘ └────────┘ └──────┘
pid ┴┴ ┴┴└───┘ ┴ ┴ └─────────┘ ┴ └──────┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
155 { rw h' at this, rcases this with ⟨c, cl, ac⟩,
id └┘ └──┘
src └─┘ └──────┘ └─────┘ └───────────────┘
typ └─┘└┘└──────┘ └─────┘└──┘└───────────────┘
doc └─┘ └──────┘ └─────┘ └───────────────┘
txt └─┘ └──────┘ └─────┘ └───────────────┘
par └─┘ └──────┘ └─────┘ └───────────────┘
pid ┴ └──────┘ ┴ └───────────────┘
st ───┘└───────────┘└────────────────────────────┘└─
156 exact ⟨c, or.inl cl, ac⟩ },
id ┴ └────┘ └┘ └┘
src └────┘ └┘└────┘┴ └┘ └┘
typ └────┘ ┴└┘└────┘┴└┘└┘└┘└┘
doc └────┘ └┘ ┴ └┘ └┘
txt └────┘ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ └┘
pid ┴ └┘ ┴ └┘ ┴┴
st ────────────────────────────┘└┘└
157 { induction e : seq.destruct S with a; rw e at h',
id └──────────┘ ┴ ┴
src └────────┘ └─┘└──────────┘┴ └─────┘ └─┘ └────┘
typ └────────┘ └─┘└──────────┘┴┴└─────┘ └─┘┴└────┘
doc └────────┘ └─┘└──────────┘┴ └─────┘ └─┘ └────┘
txt └────────┘ └─┘ ┴ └─────┘ └─┘ └────┘
par └────────┘ └─┘ ┴ └─────┘ └─┘ └────┘
pid ┴ └─┘ ┴ ┴└────┘ ┴ └────┘
st ───────────────────────────────────────────┘┴└────┘└─
158 { exact let ⟨d, o, ad⟩ := IH _ _ h',
id ┴ ┴ └┘ └┘ └┘
src └────┘ ┴ └┘ └┘ └───┘ └───┘ └─
typ └────┘ ┴ ┴└┘┴└┘└┘└───┘└┘└───┘└┘└─
doc └────┘ ┴ └┘ └┘ └───┘ └───┘ └─
txt └────┘ ┴ └┘ └┘ └───┘ └───┘ └─
par └────┘ ┴ └┘ └┘ └───┘ └───┘ └─
pid ┴ ┴ └┘ └┘ └───┘ └───┘ └─
st ─────┘└──────────────────────────────────
159 ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (not_mem_nil _), ad⟩ in
id ┴ └┘ └┘ └──┘ ┴ └────────────┘ └─────────┘
src ───────┘ └┘ └┘ └───┘ ┴ ┴ └┘ └────────────┘┴ └─────────┘└───┘ └────
typ ───────┘ ┴└┘└┘└┘└┘└───┘└──┘┴┴┴ └┘ └────────────┘┴ └─────────┘└───┘ └────
doc ───────┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ └───┘ └────
txt ───────┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ └───┘ └────
par ───────┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ └───┘ └────
pid ───────┘ └┘ └┘ └───┘ ┴ ┴ └┘ ┴ └───┘ └────
st ──────────────────────────────────────────────────────────────────────────
160 ⟨c, or.inl cl, ac⟩ },
id └────┘
src ─────┘ └┘└────┘┴ └┘ └┘
typ ─────┘ └┘└────┘┴ └┘ └┘
doc ─────┘ └┘ ┴ └┘ └┘
txt ─────┘ └┘ ┴ └┘ └┘
par ─────┘ └┘ ┴ └┘ └┘
pid ─────┘ └┘ ┴ └┘ ┴┴
st ────────────────────────┘└┘└
161 { cases a with o S', cases o with c; simp [parallel.aux1] at h';
id ┴ ┴ └───────────┘
src └────┘ └────────┘ └────┘ └─────┘ └────┘└───────────┘└─────┘
typ └────┘┴└────────┘ └────┘┴└─────┘ └────┘└───────────┘└─────┘
doc └────┘ └────────┘ └────┘ └─────┘ └────┘ └─────┘
txt └────┘ └────────┘ └────┘ └─────┘ └────┘ └─────┘
par └────┘ └────────┘ └────┘ └─────┘ └────┘ └─────┘
pid ┴ └────────┘ ┴ └─────┘ ┴┴ ┴┴└───┘
st ──────────────────────┘└─────────────────────────────────────────────
162 rcases IH _ _ h' with ⟨d, dl | dS', ad⟩,
id └┘ └┘
src └─────┘ └───┘ └─────────────────────┘
typ └─────┘└┘└───┘└┘└─────────────────────┘
doc └─────┘ └───┘ └─────────────────────┘
txt └─────┘ └───┘ └─────────────────────┘
par └─────┘ └───┘ └─────────────────────┘
pid ┴ └───┘ └─────────────────────┘
st ────────────────────────────────────────────┘└─
163 { exact let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩ in ⟨c, or.inl cl, ac⟩ },
id ┴ └┘ └┘ └──┘ ┴ ┴ └┘ └┘ └────┘
src └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘└────┘┴ └┘ └┘
typ └────┘ ┴ ┴└┘└┘└┘└┘└───┘└──┘┴┴┴ ┴└┘└┘└┘└┘└───┘ └┘└────┘┴ └┘ └┘
doc └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
pid ┴ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ ┴┴
st ───────┘└────────────────────────────────────────────────────────────────┘└┘└
164 { refine ⟨d, or.inr _, ad⟩,
id ┴ └────┘ └┘
src └─────┘ └┘└────┘└──┘ ┴
typ └─────┘ ┴└┘└────┘└──┘└┘┴
doc └─────┘ └┘ └──┘ ┴
txt └─────┘ └┘ └──┘ ┴
par └─────┘ └┘ └──┘ ┴
pid ┴ └┘ └──┘ ┴
st ───────┘└──────────────────────┘└─
165 rw seq.destruct_eq_cons e,
id └──────────────────┘ ┴
src └─┘└──────────────────┘┴
typ └─┘└──────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└─
166 exact seq.mem_cons_of_mem _ dS' },
id └─────────────────┘ └─┘
src └────┘└─────────────────┘└─┘ ┴
typ └────┘└─────────────────┘└─┘└─┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────────────────────────┘└┘└
167 { simp at dl, cases dl with dc dl,
id └┘
src └────────┘ └────┘ └─────────┘
typ └────────┘ └────┘└┘└─────────┘
doc └────────┘ └────┘ └─────────┘
txt └────────┘ └────┘ └─────────┘
par └────────┘ └────┘ └─────────┘
pid ┴└───┘ ┴ └─────────┘
st ───────┘└────────┘└───────────────────┘└─
168 { rw dc at ad, refine ⟨c, or.inr _, ad⟩,
id └┘ ┴ └────┘ └┘
src └─┘ └────┘ └─────┘ └┘└────┘└──┘ ┴
typ └─┘└┘└────┘ └─────┘ ┴└┘└────┘└──┘└┘┴
doc └─┘ └────┘ └─────┘ └┘ └──┘ ┴
txt └─┘ └────┘ └─────┘ └┘ └──┘ ┴
par └─┘ └────┘ └─────┘ └┘ └──┘ ┴
pid ┴ └────┘ ┴ └┘ └──┘ ┴
st ─────────┘└─────────┘└────────────────────────┘└─
169 rw seq.destruct_eq_cons e,
id └──────────────────┘ ┴
src └─┘└──────────────────┘┴
typ └─┘└──────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└─
170 apply seq.mem_cons },
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────┘└┘└
171 { exact let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩ in ⟨c, or.inl cl, ac⟩ } },
id ┴ └┘ └┘ └──┘ ┴ ┴ └┘ └┘ └────┘
src └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘└────┘┴ └┘ └┘
typ └────┘ ┴ ┴└┘└┘└┘└┘└───┘└──┘┴┴┴ ┴└┘└┘└┘└┘└───┘ └┘└────┘┴ └┘ └┘
doc └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ └┘
pid ┴ ┴ └┘ └┘ └───┘ ┴ ┴ └┘ └┘ └───┘ └┘ ┴ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────┘└──┘└
172 { refine ⟨d, or.inr _, ad⟩,
id ┴ └────┘ └┘
src └─────┘ └┘└────┘└──┘ ┴
typ └─────┘ ┴└┘└────┘└──┘└┘┴
doc └─────┘ └┘ └──┘ ┴
txt └─────┘ └┘ └──┘ ┴
par └─────┘ └┘ └──┘ ┴
pid ┴ └┘ └──┘ ┴
st ───────────────────────────────┘└─
173 rw seq.destruct_eq_cons e,
id └──────────────────┘ ┴
src └─┘└──────────────────┘┴
typ └─┘└──────────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└─
174 exact seq.mem_cons_of_mem _ dS' } } }
id └─────────────────┘ └─┘
src └────┘└─────────────────┘└─┘ ┴
typ └────┘└─────────────────┘└─┘└─┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────────────────────────┘└─────
175 end
st ──┘
176
177 theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map (map f)) :=
id ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴└──┘ └─┘ ┴
src └─┘ └──────┘ ┴ └──────┘ └──┘ └─┘
typ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴└──┘ └─┘ ┴
doc └─┘ └──────┘ └──────┘ └──┘ └─┘
178 begin
st └─────
179 refine eq_of_bisim (λ c1 c2, ∃ l S,
id └─────────┘ ┴ ┴
src └─────┘└─────────┘┴ └──────┘┴└──┘┴└
typ └─────┘└─────────┘┴ └──────┘┴└──┘┴└
doc └─────┘ ┴ └──────┘ └──┘ └
txt └─────┘ ┴ └──────┘ └──┘ └
par └─────┘ ┴ └──────┘ └──┘ └
pid ┴ ┴ └──────┘ └──┘ └
st ──────────────────────────────────────
180 c1 = map f (corec parallel.aux1 (l, S)) ∧
id ┴ ┴ ┴
src ───┘ ┴┴┴ ┴ ┴ ┴ ┴┴ └┘ └─┘┴└
typ ───┘ ┴┴┴ ┴ ┴ ┴ ┴┴ └┘ └─┘┴└
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ └
st ──────────────────────────────────────────────
181 c2 = corec parallel.aux1 (l.map (map f), S.map (map f))) _ ⟨[], S, rfl, rfl⟩,
id └───┘ └───────────┘ └──┘ └──┘ └─┘ ┴ ┴ └─┘
src ───┘ ┴ ┴└───┘┴└───────────┘┴ └──┘┴ ┴ └─┘ └──┘┴ └─┘┴ └────┘ └┘ └┘ └┘└─┘┴
typ ───┘ ┴ ┴└───┘┴└───────────┘┴ └──┘┴ ┴ └─┘ └──┘┴ └─┘┴┴└────┘ └┘┴└┘ └┘└─┘┴
doc ───┘ ┴ ┴└───┘┴ ┴ ┴ ┴ └─┘ └──┘┴ └─┘┴ └────┘ └┘ └┘ └┘ ┴
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ ┴
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ ┴
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────┘└─
182 intros c1 c2 h, exact match c1, c2, h with ._, ._, ⟨l, S, rfl, rfl⟩ := begin
id └┘ └┘ ┴
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───────────────┘└───────────────────────────────────────────────────────┘└─────
183 clear _match,
src ───┘└──────────┘└─
typ ───┘└──────────┘└─
doc ───┘└──────────┘└─
txt ───┘└──────────┘└─
par ───┘└──────────┘└─
pid ──────────────────
st ───────────────┘└─
184 have : parallel.aux2 (l.map (map f)) = lmap f (rmap (list.map (map f)) (parallel.aux2 l)),
id └───┘ └──┘ └──┘ └──────┘ └─┘ ┴ └───────────┘ ┴
src ───┘└─────┘ ┴ └───┘┴ ┴ └─┘ ┴└──┘┴ ┴ └──┘┴ └──────┘┴ └─┘┴ └─┘ └───────────┘┴ └┘└─
typ ───┘└─────┘ ┴ └───┘┴ ┴ └─┘ ┴└──┘┴ ┴ └──┘┴ └──────┘┴ └─┘┴┴└─┘ └───────────┘┴┴└┘└─
doc ───┘└─────┘ ┴ ┴ ┴ └─┘ ┴└──┘┴ ┴ └──┘┴ ┴ └─┘┴ └─┘ ┴ └┘└─
txt ───┘└─────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘└─
par ───┘└─────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘└─
pid ──────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
185 { simp [parallel.aux2],
id └───────────┘
src ─────┘└────┘└───────────┘┴└─
typ ─────┘└────┘└───────────┘┴└─
doc ─────┘└────┘ ┴└─
txt ─────┘└────┘ ┴└─
par ─────┘└────┘ ┴└─
pid ───────────┘ └──
st ────┘└───────────────────┘└─
186 induction l with c l IH; simp, rw [IH],
id ┴ └┘
src ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘ ┴└─
typ ─────┘└────────┘┴└──────────┘└┘└──┘└┘└──┘└┘┴└─
doc ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘ ┴└─
txt ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘ ┴└─
par ─────┘└────────┘ └──────────┘└┘└──┘└┘└──┘ ┴└─
pid ───────────────┘ └──────────────────────┘ └──
st ──────────────────────────────────┘└──────┘┴└─
187 cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l; simp [parallel.aux2],
id └────────┘ └────────────────────┘ └─────┘ └──────┘ ┴ └───────────┘
src ─────┘└────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘ └┘└────┘└───────────┘┴└─
typ ─────┘└────┘└────────┘┴└────────────────────┘┴ └─────┘┴└──────┘└┘┴└┘└────┘└───────────┘┴└─
doc ─────┘└────┘ ┴ ┴ ┴ └┘ └┘└────┘ ┴└─
txt ─────┘└────┘ ┴ ┴ ┴ └┘ └┘└────┘ ┴└─
par ─────┘└────┘ ┴ ┴ ┴ └┘ └┘└────┘ ┴└─
pid ───────────┘ ┴ ┴ ┴ └┘ └──────┘ └──
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
188 cases destruct c; simp },
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└───┘└──
typ ─────┘└────┘└──────┘┴┴└┘└───┘└──
doc ─────┘└────┘└──────┘┴ └┘└───┘└──
txt ─────┘└────┘ ┴ └┘└───┘└──
par ─────┘└────┘ ┴ └┘└───┘└──
pid ───────────┘ ┴ └─────────
st ────────────────────────────┘┴└─
189 simp [parallel.aux1], rw this, cases parallel.aux2 l with a l'; simp,
id └───────────┘ └──┘ └───────────┘ ┴
src ───┘└────┘└───────────┘┴└┘└─┘ └┘└────┘└───────────┘┴ └────────┘└┘└──┘└─
typ ───┘└────┘└───────────┘┴└┘└─┘└──┘└┘└────┘└───────────┘┴┴└────────┘└┘└──┘└─
doc ───┘└────┘ ┴└┘└─┘ └┘└────┘ ┴ └────────┘└┘└──┘└─
txt ───┘└────┘ ┴└┘└─┘ └┘└────┘ ┴ └────────┘└┘└──┘└─
par ───┘└────┘ ┴└┘└─┘ └┘└────┘ ┴ └────────┘└┘└──┘└─
pid ─────────┘ └────┘ └──────┘ ┴ └─────────────────
st ───────────────────────┘└───────┘└─────────────────────────────────────┘└─
190 apply S.cases_on _ (λ c S, _) (λ S, _); simp; simp [parallel.aux1];
id └────────┘ └───────────┘
src ───┘└────┘└────────┘└─┘ └───────┘ └────┘└┘└──┘└┘└────┘└───────────┘┴└─
typ ─────────┘└────────┘└─┘ └───────┘ └──────┘└──┘└┘└────┘└───────────┘┴└─
doc ───┘└────┘ └─┘ └───────┘ └────┘└┘└──┘└┘└────┘ ┴└─
txt ───┘└────┘ └─┘ └───────┘ └────┘└┘└──┘└┘└────┘ ┴└─
par ─────────┘ └─┘ └───────┘ └──────┘└──┘└┘└────┘ ┴└─
pid ─────────┘ └─┘ └───────┘ └──────────────────┘ └──
st ────────────────────────────────────────────────────────────────────────
191 exact ⟨_, _, rfl, rfl⟩
id └─┘
src ─────────┘ └────┘ └┘└─┘└─
typ ─────────┘ └────┘ └┘└─┘└─
doc ─────────┘ └────┘ └┘ └─
txt ─────────┘ └────┘ └┘ └─
par ─────────┘ └────┘ └┘ └─
pid ─────────┘ └────┘ └┘ └─
st ───────────────────────────
192 end end
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ────────┘┴
st ─┘└─┘└───┘
193 end
st └─┘
194
195 theorem parallel_empty (S : wseq (computation α)) (h : S.head ~> none) :
id └──┘ └─────────┘ ┴ ┴└───┘ └┘ └──┘
src └──┘ └─────────┘ └───┘ └┘ └──┘
typ └──┘ └─────────┘ ┴ ┴└───┘ └┘ └──┘
doc └──┘ └─────────┘ └───┘ └┘
196 parallel S = empty _ :=
id └──────┘ ┴ ┴ └───┘
src └──────┘ ┴ └───┘
typ └──────┘ ┴ ┴ └───┘
doc └──────┘ └───┘
197 eq_empty_of_not_terminates $ λ ⟨a, m⟩,
id └────────────────────────┘ ┴ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴ ┴
198 let ⟨c, cs, ac⟩ := exists_of_mem_parallel m,
id └─┘ └┘ └────────────────────┘
src └────────────────────┘
typ └─┘ └┘ └────────────────────┘
199 ⟨n, nm⟩ := exists_nth_of_mem cs,
id └┘ └───────────────┘
src └───────────────┘
typ └┘ └───────────────┘
200 ⟨c', h'⟩ := head_some_of_nth_some nm in by injection h h'
id └───────────────────┘ ┴ └┘
src └───────────────────┘ └────────┘ ┴ └
typ └───────────────────┘ └────────┘┴┴└┘└
doc └────────┘ ┴ └
txt └────────┘ ┴ └
par └────────┘ ┴ └
pid ┴ ┴ └
st └───────────────
201
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
202 -- The reason this isn't trivial from exists_of_mem_parallel is because it eliminates to Sort
src ─────────────────────────────────────────────────────────────────────────────────────────────┘
typ ─────────────────────────────────────────────────────────────────────────────────────────────┘
doc ─────────────────────────────────────────────────────────────────────────────────────────────┘
txt ─────────────────────────────────────────────────────────────────────────────────────────────┘
par ─────────────────────────────────────────────────────────────────────────────────────────────┘
pid ─────────────────────────────────────────────────────────────────────────────────────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────────────┘
203 def parallel_rec {S : wseq (computation α)} (C : α → Sort v)
id └──┘ └─────────┘ ┴ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴ ┴
doc └──┘ └─────────┘
204 (H : ∀ s ∈ S, ∀ a ∈ s, C a) {a} (h : a ∈ parallel S) : C a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
205 begin
st └─────
206 let T : wseq (computation (α × computation α)) :=
id └──┘ ┴ └─────────┘ ┴
src └──────┘└──┘┴ ┴ ┴┴┴└─────────┘┴ └─────
typ └──────┘└──┘┴ ┴ ┴┴┴└─────────┘┴┴└─────
doc └──────┘└──┘┴ ┴ ┴ ┴└─────────┘┴ └─────
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └─────
par └──────┘ ┴ ┴ ┴ ┴ ┴ └─────
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ └┘└───
st ────────────────────────────────────────────────────
207 S.map (λc, c.map (λ a, (a, c))),
id └───┘ └──┘
src ───┘└───┘┴ └─┘ └──┘┴ └──┘ └┘ └─┘
typ ───┘└───┘┴ └─┘ └──┘┴ └──┘ └┘ └─┘
doc ───┘└───┘┴ └─┘ └──┘┴ └──┘ └┘ └─┘
txt ───┘ ┴ └─┘ ┴ └──┘ └┘ └─┘
par ───┘ ┴ └─┘ ┴ └──┘ └┘ └─┘
pid ───┘ ┴ └─┘ ┴ └──┘ └┘ └─┘
st ──────────────────────────────────┘└─
208 have : S = T.map (map (λ c, c.1)),
id ┴ ┴ └───┘ └─┘
src └─────┘ ┴┴┴└───┘┴ └─┘┴ └──┘ └──┘
typ └─────┘┴┴┴┴└───┘┴ └─┘┴ └──┘ └──┘
doc └─────┘ ┴ ┴└───┘┴ └─┘┴ └──┘ └──┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └──┘
st ──────────────────────────────────┘└─
209 { rw [←wseq.map_comp], refine (wseq.map_id _).symm.trans (congr_arg (λ f, wseq.map f S) _),
id └───────────┘ └─────────┘ └───────┘ └──────┘ ┴
src └───┘└───────────┘┴ └─────┘ └─────────┘└─────────────┘ └───────┘┴ └──┘└──────┘┴ ┴ └──┘
typ └───┘└───────────┘┴ └─────┘ └─────────┘└─────────────┘ └───────┘┴ └──┘└──────┘┴ ┴┴└──┘
doc └───┘ ┴ └─────┘ └─────────────┘ ┴ └──┘└──────┘┴ ┴ └──┘
txt └───┘ ┴ └─────┘ └─────────────┘ ┴ └──┘ ┴ ┴ └──┘
par └───┘ ┴ └─────┘ └─────────────┘ ┴ └──┘ ┴ ┴ └──┘
pid └─┘ ┴ ┴ └─────────────┘ ┴ └──┘ ┴ ┴ └──┘
st ───┘└────────────────┘└────────────────────────────────────────────────────────────────────┘└─
210 funext c, dsimp [id, function.comp], rw [←map_comp], exact (map_id _).symm },
id └┘ └───────────┘ └──────┘ └────┘
src └──────┘ └─────┘└┘└┘└───────────┘┴ └───┘└──────┘┴ └────┘ └────┘└───────┘
typ └──────┘ └─────┘└┘└┘└───────────┘┴ └───┘└──────┘┴ └────┘ └────┘└───────┘
doc └──────┘ └─────┘ └┘ ┴ └───┘ ┴ └────┘ └───────┘
txt └──────┘ └─────┘ └┘ ┴ └───┘ ┴ └────┘ └───────┘
par └──────┘ └─────┘ └┘ ┴ └───┘ ┴ └────┘ └───────┘
pid └┘ ┴┴ └┘ ┴ └─┘ ┴ ┴ └─────┘└┘
st ───────────┘└─────────────────────────┘└─────────────┘└───────────────────────┘└┘└
211 have pe := congr_arg parallel this, rw ←map_parallel at pe,
id └───────┘ └──────┘ └──┘ └──────────┘
src └─────────┘└───────┘┴└──────┘┴ └──┘└──────────┘└────┘
typ └─────────┘└───────┘┴└──────┘┴└──┘ └──┘└──────────┘└────┘
doc └─────────┘ ┴└──────┘┴ └──┘ └────┘
txt └─────────┘ ┴ ┴ └──┘ └────┘
par └─────────┘ ┴ ┴ └──┘ └────┘
pid └─────┘┴└─┘ ┴ ┴ └┘ └────┘
st ───────────────────────────────────┘└──────────────────────┘└─
212 have h' := h, rw pe at h',
id ┴ └┘
src └─────────┘ └─┘ └────┘
typ └─────────┘┴ └─┘└┘└────┘
doc └─────────┘ └─┘ └────┘
txt └─────────┘ └─┘ └────┘
par └─────────┘ └─┘ └────┘
pid └─────┘┴└─┘ ┴ └────┘
st ─────────────┘└───────────┘└─
213 haveI : terminates (parallel T) := (terminates_map_iff _ _).1 ⟨_, h'⟩,
id └────────┘ └──────┘ ┴ └────────────────┘ └┘
src └──────┘└────────┘┴ └──────┘┴ └───┘ └────────────────┘└──────┘ └─┘ ┴
typ └──────┘└────────┘┴ └──────┘┴┴└───┘ └────────────────┘└──────┘ └─┘└┘┴
doc └──────┘└────────┘┴ └──────┘┴ └───┘ └──────┘ └─┘ ┴
txt └──────┘ ┴ ┴ └───┘ └──────┘ └─┘ ┴
par └──────┘ ┴ ┴ └───┘ └──────┘ └─┘ ┴
pid ┴└┘ ┴ ┴ ┴└──┘ └──────┘ └─┘ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
214 induction e : get (parallel T) with a' c,
id └─┘ └──────┘ ┴
src └────────┘ └─┘└─┘┴ └──────┘┴ └─────────┘
typ └────────┘ └─┘└─┘┴ └──────┘┴┴└─────────┘
doc └────────┘ └─┘└─┘┴ └──────┘┴ └─────────┘
txt └────────┘ └─┘ ┴ ┴ └─────────┘
par └────────┘ └─┘ ┴ ┴ └─────────┘
pid ┴ └─┘ ┴ ┴ ┴┴└───────┘
st ─────────────────────────────────────────┘└─
215 have : a ∈ c ∧ c ∈ S,
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴┴┴ ┴┴┴ ┴ ┴
typ └─────┘┴┴┴┴ ┴┴┴┴┴ ┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────┘└─
216 { rcases exists_of_mem_map h' with ⟨d, dT, cd⟩,
id └───────────────┘ └┘
src └─────┘└───────────────┘┴ └───────────────┘
typ └─────┘└───────────────┘┴└┘└───────────────┘
doc └─────┘ ┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ───┘└──────────────────────────────────────────┘└─
217 rw get_eq_of_mem _ dT at e, cases e, dsimp at cd, cases cd,
id └───────────┘ └┘ ┴ └┘
src └─┘└───────────┘└─┘ └───┘ └────┘ └─────────┘ └────┘
typ └─┘└───────────┘└─┘└┘└───┘ └────┘┴ └─────────┘ └────┘└┘
doc └─┘ └─┘ └───┘ └────┘ └─────────┘ └────┘
txt └─┘ └─┘ └───┘ └────┘ └─────────┘ └────┘
par └─┘ └─┘ └───┘ └────┘ └─────────┘ └────┘
pid ┴ └─┘ └───┘ ┴ ┴└───┘ ┴
st ─────────────────────────────┘└───────┘└───────────┘└────────┘└─
218 rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩,
id └────────────────────┘ └┘
src └─────┘└────────────────────┘┴ └──────────────────┘
typ └─────┘└────────────────────┘┴└┘└──────────────────┘
doc └─────┘ ┴ └──────────────────┘
txt └─────┘ ┴ └──────────────────┘
par └─────┘ ┴ └──────────────────┘
pid ┴ ┴ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
219 rcases wseq.exists_of_mem_map dT' with ⟨c', cs', e'⟩,
id └────────────────────┘ └─┘
src └─────┘└────────────────────┘┴ └─────────────────┘
typ └─────┘└────────────────────┘┴└─┘└─────────────────┘
doc └─────┘ ┴ └─────────────────┘
txt └─────┘ ┴ └─────────────────┘
par └─────┘ ┴ └─────────────────┘
pid ┴ ┴ └─────────────────┘
st ───────────────────────────────────────────────────────┘└─
220 rw ←e' at ad',
id └┘
src └──┘ └─────┘
typ └──┘└┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid └┘ └─────┘
st ────────────────┘└─
221 rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩, injection e' with i1 i2,
id └───────────────┘ └─┘ └┘
src └─────┘└───────────────┘┴ └─────────────────┘ └────────┘ └─────────┘
typ └─────┘└───────────────┘┴└─┘└─────────────────┘ └────────┘└┘└─────────┘
doc └─────┘ ┴ └─────────────────┘ └────────┘ └─────────┘
txt └─────┘ ┴ └─────────────────┘ └────────┘ └─────────┘
par └─────┘ ┴ └─────────────────┘ └────────┘ └─────────┘
pid ┴ ┴ └─────────────────┘ ┴ └─────────┘
st ──────────────────────────────────────────────────┘└───────────────────────┘└─
222 constructor, rwa [i1, i2] at ac', rwa i2 at cs' },
id └┘ └┘ └┘
src └─────────┘ └───┘ └┘ └──────┘ └──┘ └──────┘
typ └─────────┘ └───┘└┘└┘└┘└──────┘ └──┘└┘└──────┘
doc └─────────┘ └───┘ └┘ └──────┘ └──┘ └──────┘
txt └─────────┘ └───┘ └┘ └──────┘ └──┘ └──────┘
par └─────────┘ └───┘ └┘ └──────┘ └──┘ └──────┘
pid └┘ └┘ ┴└─────┘ ┴ └─────┘┴
st ──────────────┘└───────┘└──┘┴└─────┘└──────────────┘└┘└
223 cases this with ac cs, apply H _ cs _ ac
id └──┘ ┴ └┘ └┘
src └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴
typ └────┘└──┘└─────────┘ └────┘┴└─┘└┘└─┘└┘┴
doc └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴
txt └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴
par └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴
pid ┴ └─────────┘ ┴ └─┘ └─┘ ┴
st ──────────────────────┘└──────────────────┘
224 end
st └─┘
225
226 theorem parallel_promises {S : wseq (computation α)} {a}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
227 (H : ∀ s ∈ S, s ~> a) : parallel S ~> a :=
id ┴ ┴ ┴ └┘ ┴ └──────┘ ┴ └┘ ┴
src └┘ └──────┘ └┘
typ ┴ ┴ ┴ └┘ ┴ └──────┘ ┴ └┘ ┴
doc └┘ └──────┘ └┘
228 λ a' ma', let ⟨c, cs, ac⟩ := exists_of_mem_parallel ma' in H _ cs ac
id └┘ └─┘ └─┘ └┘ └┘ └────────────────────┘ └─┘ ┴
src └────────────────────┘
typ └┘ └─┘ └─┘ └┘ └┘ └────────────────────┘ └─┘ ┴
229
230 theorem mem_parallel {S : wseq (computation α)} {a}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
231 (H : ∀ s ∈ S, s ~> a) {c} (cs : c ∈ S) (ac : a ∈ c) : a ∈ parallel S :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
src └┘ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └┘ └──────┘
232 by haveI := terminates_of_mem ac; have := terminates_parallel cs;
id └───────────────┘ └┘ └─────────────────┘ └┘
src └───────┘└───────────────┘┴ └──────┘└─────────────────┘┴
typ └───────┘└───────────────┘┴└┘ └──────┘└─────────────────┘┴└┘
doc └───────┘ ┴ └──────┘ ┴
txt └───────┘ ┴ └──────┘ ┴
par └───────┘ ┴ └──────┘ ┴
pid ┴└─┘ ┴ └───┘└─┘ ┴
st └───────────────────────────────────────────────────────────────
233 exact mem_of_promises _ (parallel_promises H)
id └─────────────┘ └───────────────┘ ┴
src └────┘└─────────────┘└─┘ └───────────────┘┴ └─
typ └────┘└─────────────┘└─┘ └───────────────┘┴┴└─
doc └────┘ └─┘ ┴ └─
txt └────┘ └─┘ ┴ └─
par └────┘ └─┘ ┴ └─
pid ┴ └─┘ ┴ ┴└
st ─────────────────────────────────────────────────
234
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
235 theorem parallel_congr_lem {S T : wseq (computation α)} {a}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
236 (H : S.lift_rel equiv T) : (∀ s ∈ S, s ~> a) ↔ (∀ t ∈ T, t ~> a) :=
id ┴└───────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └───────┘ └───┘ └┘ ┴ └┘
typ ┴└───────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └───────┘ └───┘ └┘ └┘
237 ⟨λ h1 t tT, let ⟨s, sS, se⟩ := wseq.exists_of_lift_rel_right H tT in
id └┘ ┴ └┘ └─┘ └┘ └┘ └───────────────────────────┘ ┴ └┘
src └───────────────────────────┘
typ └┘ ┴ └┘ └─┘ └┘ └┘ └───────────────────────────┘ ┴ └┘
238 (promises_congr se _).1 (h1 _ sS),
id └────────────┘ ┴ └┘
src └────────────┘ ┴
typ └────────────┘ ┴ └┘
239 λ h2 s sS, let ⟨t, tT, se⟩ := wseq.exists_of_lift_rel_left H sS in
id └┘ ┴ └┘ └─┘ └┘ └┘ └──────────────────────────┘ ┴ └┘
src └──────────────────────────┘
typ └┘ ┴ └┘ └─┘ └┘ └┘ └──────────────────────────┘ ┴ └┘
240 (promises_congr se _).2 (h2 _ tT)⟩
id └────────────┘ ┴ └┘
src └────────────┘ ┴
typ └────────────┘ ┴ └┘
241
242 -- The parallel operation is only deterministic when all computation paths lead to the same value
243 theorem parallel_congr_left {S T : wseq (computation α)} {a}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
244 (h1 : ∀ s ∈ S, s ~> a) (H : S.lift_rel equiv T) : parallel S ~ parallel T :=
id ┴ ┴ ┴ └┘ ┴ ┴└───────┘ └───┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ └───────┘ └───┘ └──────┘ ┴ └──────┘
typ ┴ ┴ ┴ └┘ ┴ ┴└───────┘ └───┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └───────┘ └───┘ └──────┘ ┴ └──────┘
245 let h2 := (parallel_congr_lem H).1 h1 in
id └┘ └────────────────┘ ┴ ┴ └┘
src └────────────────┘ ┴
typ └┘ └────────────────┘ ┴ ┴ └┘
246 λ a', ⟨λh, by have aa := parallel_promises h1 h; rw ←aa; rw ←aa at h; exact
id └┘ ┴ └───────────────┘ └┘ ┴ └┘ └┘
src └─────────┘└───────────────┘┴ ┴ └──┘ └──┘ └───┘ └─────
typ └┘ ┴ └─────────┘└───────────────┘┴└┘┴┴ └──┘└┘ └──┘└┘└───┘ └─────
doc └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
txt └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
par └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
pid └─────┘┴└─┘ ┴ ┴ └┘ └┘ └───┘ └
st └──────────────────────────────────────────────────────────────
247 let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
id └┘ └┘ └────────────────────┘ ┴
src ─┘ ┴ └┘ └┘ └───┘└────────────────────┘┴ └─
typ ─┘ ┴ └┘└┘└┘└┘└───┘└────────────────────┘┴┴└─
doc ─┘ ┴ └┘ └┘ └───┘ ┴ └─
txt ─┘ ┴ └┘ └┘ └───┘ ┴ └─
par ─┘ ┴ └┘ └┘ └───┘ ┴ └─
pid ─┘ ┴ └┘ └┘ └───┘ ┴ └─
st ───────────────────────────────────────────────
248 ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_left H sS,
id └┘ └┘ └──────────────────────────┘ ┴
src ─────┘ └┘ └┘ └───┘└──────────────────────────┘┴ ┴ └─
typ ─────┘ └┘└┘└┘└┘└───┘└──────────────────────────┘┴┴┴ └─
doc ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
txt ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
par ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
pid ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
st ────────────────────────────────────────────────────────
249 aT := (st _).1 as in mem_parallel h2 tT aT,
id └──────────┘ └┘
src ───────────┘ └────┘ └──┘└──────────┘┴ ┴ ┴
typ ───────────┘ └────┘ └──┘└──────────┘┴└┘┴ ┴
doc ───────────┘ └────┘ └──┘ ┴ ┴ ┴
txt ───────────┘ └────┘ └──┘ ┴ ┴ ┴
par ───────────┘ └────┘ └──┘ ┴ ┴ ┴
pid ───────────┘ └────┘ └──┘ ┴ ┴ ┴
st ───────────────────────────────────────────────┘
250 λh, by have aa := parallel_promises h2 h; rw ←aa; rw ←aa at h; exact
id ┴ └───────────────┘ └┘ ┴ └┘ └┘
src └─────────┘└───────────────┘┴ ┴ └──┘ └──┘ └───┘ └─────
typ ┴ └─────────┘└───────────────┘┴└┘┴┴ └──┘└┘ └──┘└┘└───┘ └─────
doc └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
txt └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
par └─────────┘ ┴ ┴ └──┘ └──┘ └───┘ └─────
pid └─────┘┴└─┘ ┴ ┴ └┘ └┘ └───┘ └
st └──────────────────────────────────────────────────────────────
251 let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
id └┘ └┘ └────────────────────┘ ┴
src ─┘ ┴ └┘ └┘ └───┘└────────────────────┘┴ └─
typ ─┘ ┴ └┘└┘└┘└┘└───┘└────────────────────┘┴┴└─
doc ─┘ ┴ └┘ └┘ └───┘ ┴ └─
txt ─┘ ┴ └┘ └┘ └───┘ ┴ └─
par ─┘ ┴ └┘ └┘ └───┘ ┴ └─
pid ─┘ ┴ └┘ └┘ └───┘ ┴ └─
st ───────────────────────────────────────────────
252 ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_right H sS,
id └┘ └┘ └───────────────────────────┘ ┴
src ─────┘ └┘ └┘ └───┘└───────────────────────────┘┴ ┴ └─
typ ─────┘ └┘└┘└┘└┘└───┘└───────────────────────────┘┴┴┴ └─
doc ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
txt ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
par ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
pid ─────┘ └┘ └┘ └───┘ ┴ ┴ └─
st ─────────────────────────────────────────────────────────
253 aT := (st _).2 as in mem_parallel h1 tT aT⟩
id └──────────┘ └┘
src ───────────┘ └────┘ └──┘└──────────┘┴ ┴ ┴
typ ───────────┘ └────┘ └──┘└──────────┘┴└┘┴ ┴
doc ───────────┘ └────┘ └──┘ ┴ ┴ ┴
txt ───────────┘ └────┘ └──┘ ┴ ┴ ┴
par ───────────┘ └────┘ └──┘ ┴ ┴ ┴
pid ───────────┘ └────┘ └──┘ ┴ ┴ ┴
st ───────────────────────────────────────────────┘
254
255 theorem parallel_congr_right {S T : wseq (computation α)} {a}
id └──┘ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ └─────────┘ ┴
doc └──┘ └─────────┘
256 (h2 : ∀ t ∈ T, t ~> a) (H : S.lift_rel equiv T) : parallel S ~ parallel T :=
id ┴ ┴ ┴ └┘ ┴ ┴└───────┘ └───┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ └───────┘ └───┘ └──────┘ ┴ └──────┘
typ ┴ ┴ ┴ └┘ ┴ ┴└───────┘ └───┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └───────┘ └───┘ └──────┘ ┴ └──────┘
257 parallel_congr_left ((parallel_congr_lem H).2 h2) H
id └─────────────────┘ └────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘ └────────────────┘ ┴
typ └─────────────────┘ └────────────────┘ ┴ ┴ └┘ ┴
258
259 end computation